package river_city_ransom.contracts;

import java.util.ArrayList;
import java.util.List;

import exceptions.ComposantError;
import exceptions.InvariantError;
import exceptions.PostconditionError;
import exceptions.PreconditionError;
import river_city_ransom.services.Dimensions;
import river_city_ransom.services.Equipable;
import river_city_ransom.services.Objet;
import river_city_ransom.services.PersonnageJouable;
import river_city_ransom.services.Position;
import tools.Toolbox;


public class PersonnageJouable_C extends Personnage_C implements PersonnageJouable {
	public PersonnageJouable_C(PersonnageJouable delegate) {
		super(delegate);
	}
	
	@Override
	protected PersonnageJouable delegate() {
		return (PersonnageJouable) super.delegate();
	}
	
	/** __________________________________________________________ INVARIANTS */
	public void checkInvariants() throws ComposantError {
		super.checkInvariants();
		
		boolean inv;
//		inv sommeDArgent(P) >= 0
		inv = sommeDArgent() >= 0;
		if(!inv) {
			throw new InvariantError("sommeDArgent(P) >= 0");
		}
	}
	
	/** _________________________________________________________ OBSERVATORS */
	@Override
	public int sommeDArgent() {
		return delegate().sommeDArgent();
	}
	
	@Override
	public List<Objet> poche() {
		return delegate().poche();
	}
	
	/** ________________________________________________________ CONSTRUCTORS */
	@Override
	public void init(String n, Dimensions d, int f, int pv) throws ComposantError {
		boolean pre;
//		pre init(n, d, f, pv) require n != "" ^ d != NULL ^ f > 0 ^ pv > 0
		pre = n != null && !Toolbox.equals(n, "") && d != null && f > 0 && pv > 0;
		if(!pre) {
			throw new PreconditionError("init(n, d, f, pv) require n != \"\" ^ d != NULL ^ f > 0 ^ pv > 0");
		}
		
		delegate().init(n, d, f, pv);
		
		checkInvariants();
		
		boolean post;
//		post nom(init(n, d, f, pv)) = n
		post = Toolbox.equals(nom(), n);
		if(!post) {
			throw new PostconditionError("nom(init(n, d, f, pv)) = n");
		}
//		post dimensions(init(n, d, f, pv)) = d
		post = Toolbox.equals(dimensions(), d);
		if(!post) {
			throw new PostconditionError("dimensions(init(n, d, f, pv)) = d");
		}
//		post estPorte(init(n, d, f, pv)) = false
		post = estPorte() == false;
		if(!post) {
			throw new PostconditionError("estPorte(init(n, d, f, pv)) = false");
		}
//		post estJete(init(n, d, f, pv)) = 0
		post = estJete() == 0;
		if(!post) {
			throw new PostconditionError("estJete(init(n, d, f, pv)) = 0");
		}
//		post force(init(n, d, f, pv)) = f
		post = force() == f;
		if(!post) {
			throw new PostconditionError("force(init(n, d, f, pv)) = f");
		}
//		post maxPointsDeVie(init(n, d, f, pv)) = pv
		post = maxPointsDeVie() == pv;
		if(!post) {
			throw new PostconditionError("maxPointsDeVie(init(n, d, f, pv)) = pv");
		}
//		post pointsDeVie(init(n, d, f, pv)) = pv
		post = pointsDeVie() == pv;
		if(!post) {
			throw new PostconditionError("pointsDeVie(init(n, d, f, pv)) = pv");
		}
//		post choseEquipee(init(n, d, f, pv)) = NULL
		post = choseEquipee() == null;
		if(!post) {
			throw new PostconditionError("choseEquipee(init(n, d, f, pv)) = NULL");
		}
//		post position(init(n, d, f, pv)) = Position::init(0, 0, 0)
		Position p_init = position();
		p_init.init(0, 0, 0);
		post = Toolbox.equals(position(), p_init);
		if(!post) {
			throw new PostconditionError("position(init(n, d, f, pv)) = Position::init(0, 0, 0)");
		}
//		post estGele(init(n, d, f, pv)) = 0
		post = estGele() == 0;
		if(!post) {
			throw new PostconditionError("estGele(init(n, d, f, pv)) = 0");
		}
//		post versLaDroite(init(n, d, f, pv)) = true
		post = versLaDroite() == true;
		if(!post) {
			throw new PostconditionError("versLaDroite(init(n, d, f, pv)) = true");
		}
//		post sommeDArgent(init(n, d, f, pv)) = 0
		post = sommeDArgent() == 0;
		if(!post) {
			throw new PostconditionError("sommeDArgent(init(n, d, f, pv)) = 0");
		}
//		post poche(init(n, d, f, pv)) = Ø
		post = poche().size() == 0;
		if(!post) {
			throw new PostconditionError("poche(init(n, d, f, pv)) = Ø");
		}
	}
	
	/** ___________________________________________________________ OPERATORS */
	@Override
	public void deposerArgent(int a) throws ComposantError {
		boolean pre;
//		pre deposerArgent(P, a) require a > 0
		pre = a > 0;
		if(!pre) {
			throw new PreconditionError("deposerArgent(P, a) require a > 0");
		}
		
		int sa_pre = sommeDArgent();
		List<Objet> lp_pre = new ArrayList<Objet>(poche());
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Equipable ce_pre = choseEquipee();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();

		checkInvariants();
		
		delegate().deposerArgent(a);
		
		checkInvariants();
		
		boolean post;
//		post sommeDArgent(deposerArgent(P, a)) = sommeDArgent(P) + a
		post = sommeDArgent() == sa_pre + a;
		if(!post) {
			throw new PostconditionError("sommeDArgent(deposerArgent(P, a)) = sommeDArgent(P) + a");
		}
//		post poche(deposerArgent(P, a)) = poche(P)
		post = Toolbox.equals(poche(), lp_pre);
		if(!post) {
			throw new PostconditionError("poche(deposerArgent(P, a)) = poche(P)");
		}
//		post pointsDeVie(deposerArgent(P, a)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(deposerArgent(P, a)) = pointsDeVie(P)");
		}
//		post estPorte(deposerArgent(P, a)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(deposerArgent(P, a)) = estPorte(P)");
		}
//		post estJete(deposerArgent(P, a)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(deposerArgent(P, a)) = estJete(P)");
		}
//		post choseEquipee(deposerArgent(P, a)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(deposerArgent(P, a)) = choseEquipee(P)");
		}
//		post position(deposerArgent(P, a)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(deposerArgent(P, a)) = position(P)");
		}
//		post versLaDroite(deposerArgent(P, a)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(deposerArgent(P, a)) = versLaDroite(P)");
		}
//		post estGele(deposerArgent(P, a)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(deposerArgent(P, a)) = estGele(P)");
		}
	}
	
	@Override
	public void retirerArgent(int a) throws ComposantError {
		boolean pre;
//		pre retirerArgent(P, a) require sommeDArgent(P) >= a > 0
		pre = sommeDArgent() >= a && a > 0;
		if(!pre) {
			throw new PreconditionError("retirerArgent(P, a) require sommeDArgent(P) >= a > 0");
		}
		
		int sa_pre = sommeDArgent();
		List<Objet> lp_pre = new ArrayList<Objet>(poche());
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Equipable ce_pre = choseEquipee();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();

		checkInvariants();
		
		delegate().retirerArgent(a);
		
		checkInvariants();
		
		boolean post;
//		post sommeDArgent(retirerArgent(P, a)) = sommeDArgent(P) - a
		post = sommeDArgent() == sa_pre - a;
		if(!post) {
			throw new PostconditionError("sommeDArgent(retirerArgent(P, a)) = sommeDArgent(P) - a");
		}
//		post poche(retirerArgent(P, a)) = poche(P)
		post = Toolbox.equals(poche(), lp_pre);
		if(!post) {
			throw new PostconditionError("poche(retirerArgent(P, a)) = poche(P)");
		}
//		post pointsDeVie(retirerArgent(P, a)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(retirerArgent(P, a)) = pointsDeVie(P)");
		}
//		post estPorte(retirerArgent(P, a)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(retirerArgent(P, a)) = estPorte(P)");
		}
//		post estJete(retirerArgent(P, a)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(retirerArgent(P, a)) = estJete(P)");
		}
//		post choseEquipee(retirerArgent(P, a)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(retirerArgent(P, a)) = choseEquipee(P)");
		}
//		post position(retirerArgent(P, a)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(retirerArgent(P, a)) = position(P)");
		}
//		post versLaDroite(retirerArgent(P, a)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(retirerArgent(P, a)) = versLaDroite(P)");
		}
//		post estGele(retirerArgent(P, a)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(retirerArgent(P, a)) = estGele(P)");
		}
	}

	@Override
	public void ranger(Objet o) throws ComposantError {
		boolean pre;
//		pre ranger(P, O) require !estVaincu(P) ^ estGele(P) = 0 ^ estMarchandable(O)
		pre = !estVaincu() && estGele() == 0 && o.estMarchandable();
		if(!pre) {
			throw new PreconditionError("ranger(P, O) require !estVaincu(P) ^ estGele(P) = 0 ^ estMarchandable(O)");
		}
		
		int sa_pre = sommeDArgent();
		List<Objet> lp_pre = new ArrayList<Objet>(poche());
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Equipable ce_pre = choseEquipee();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();

		checkInvariants();
		
		delegate().ranger(o);
		
		checkInvariants();
		
		boolean post;
//		post poche(ranger(P, O)) = {poche(P) ∪ O}
		lp_pre.add(o);
		post = Toolbox.equals(poche(), lp_pre);
		if(!post) {
			throw new PostconditionError("poche(ranger(P, O)) = {poche(P) ∪ O}");
		}
//		post sommeDArgent(ranger(P, O)) = sommeDArgent(P)
		post = sommeDArgent() == sa_pre;
		if(!post) {
			throw new PostconditionError("sommeDArgent(ranger(P, O)) = sommeDArgent(P)");
		}
//		post pointsDeVie(ranger(P, O)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(ranger(P, O)) = pointsDeVie(P)");
		}
//		post estPorte(ranger(P, O)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(ranger(P, O)) = estPorte(P)");
		}
//		post estJete(ranger(P, O)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(ranger(P, O)) = estJete(P)");
		}
//		post choseEquipee(ranger(P, O)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(ranger(P, O)) = choseEquipee(P)");
		}
//		post position(ranger(P, O)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(ranger(P, O)) = position(P)");
		}
//		post versLaDroite(ranger(P, O)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(ranger(P, O)) = versLaDroite(P)");
		}
//		post estGele(ranger(P, O)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(ranger(P, O)) = estGele(P)");
		}
	}
	
	@Override
	public void vendre(Objet o) throws ComposantError {
		boolean pre;
//		pre vendre(P, O) require !estVaincu(P) ^ estGele(P) = 0 ^ O ∈ poche(P)
		pre = !estVaincu() && estGele() == 0 && poche().contains(o);
		if(!pre) {
			throw new PreconditionError("vendre(P, O) require !estVaincu(P) ^ estGele(P) = 0 ^ O ∈ poche(P)");
		}
		
		int sa_pre = sommeDArgent();
		List<Objet> lp_pre = new ArrayList<Objet>(poche());
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Equipable ce_pre = choseEquipee();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();

		checkInvariants();
		
		delegate().vendre(o);
		
		checkInvariants();
		
		boolean post;
//		post poche(vendre(P, O)) = {poche(P) \ O}
		lp_pre.remove(o);
		post = Toolbox.equals(poche(), lp_pre);
		if(!post) {
			throw new PostconditionError("poche(vendre(P, O)) = {poche(P) \\ O}");
		}
//		post sommeDArgent(vendre(P, O)) = sommeDArgent(P) + Objet::valeur(O)
		post = sommeDArgent() == sa_pre + o.valeur();
		if(!post) {
			throw new PostconditionError("sommeDArgent(vendre(P, O)) = sommeDArgent(P) + Objet::valeur(O)");
		}
//		post pointsDeVie(vendre(P, O)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(vendre(P, O)) = pointsDeVie(P)");
		}
//		post estPorte(vendre(P, O)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(vendre(P, O)) = estPorte(P)");
		}
//		post estJete(vendre(P, O)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(vendre(P, O)) = estJete(P)");
		}
//		post choseEquipee(vendre(P, O)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(vendre(P, O)) = choseEquipee(P)");
		}
//		post position(vendre(P, O)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(vendre(P, O)) = position(P)");
		}
//		post versLaDroite(vendre(P, O)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(vendre(P, O)) = versLaDroite(P)");
		}
//		post estGele(vendre(P, O)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(vendre(P, O)) = estGele(P)");
		}
	}
}
